g:GrpSig, b:, x:|g|. (b)  ((when b. x) = x) 

latex

Up	groups 1
Definitions of Statement	when b. p
Definitions	, ff, tt, t  T, if b then t else f fi , when b. p, P  Q, x:A. B(x), False, A, P & Q, P  Q, Unit, ,
Lemmas	grp sig wf, grp car wf, assert of bnot, eqff to assert, not wf, bnot wf, assert wf, iff transitivity, eqtt to assert, bool wf